Section: Partnerships and Cooperations

International Initiatives

Visits of International Scientists

• D. Ishii (National Institute of Informatics, Japan) visited the team for 8 months to work on applying program verification methods to hybrid systems.

Supervision of Post-docs and Internships

• S. Boldo supervised the 6-month post-doc intern of E. Makarov (from University of Vermont, USA) about numerical analysis proofs in higher dimensions.

• C. Marché supervised the post-doc intern of K. Krishnamani (from University of Trento, Italy) until August: predicate abstraction techniques for critical C programs ([38] http://proval.lri.fr/agen ).

• S. Conchon and G. Melquiond supervise the post-doc intern of Cody Roux since May 2011: integration of the Gappa theorem prover in the Alt-Ergo SMT solver.

• S. Conchon supervises the post-doc intern of D. Cousineau since October 2011: interpretation of Alt-Ergo's proof traces in the Coq proof assistant.

• C. Paulin supervised the internship of N. Gaspar (Universidade da Beira Interior, Portugal) from January to September 2011. He studied the formal proof of concurrent programs using a rely-guarantee approach.

• E. Contejean, together with V. Benzaken (LRI), supervise the internship of S. Yuan (Zhejiang University, China) from October 2011 to March 2012: Automated constraints verification for databases with SMT solvers.

Participation In International Programs

C. Paulin is the representative of Univ. Paris-Sud for the education part of the EIT KIC ICT Labs. She contributed to the proposition of two master programs as well as the action on weaving Innovation and Entrepreneurship in Doctoral programs and the preparation of the SummerSchool “Imagine the future in ICT”.